\begin{tabbing}
$\forall$$a$:Id, $T$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]$T$
\\[0ex]$\Rightarrow$ AtomFree(Type;$T$)
\\[0ex]$\Rightarrow$ $\forall$$x$$\in$dom(${\it ds}$). $A$=${\it ds}$($x$) $\Rightarrow$  $A$
\\[0ex]$\Rightarrow$ $\forall$$x$$\in$dom(${\it ds}$). $A$=${\it ds}$($x$) $\Rightarrow$  AtomFree(Type;$A$)
\\[0ex]$\Rightarrow$ ($\forall$$s$:State(${\it ds}$). Dec($\exists$$v$:$T$. $P$($s$,$v$)))
\\[0ex]$\Rightarrow$ F\=easible((with ds: ${\it ds}$\+
\\[0ex]action $a$:$T$
\\[0ex]precondition $a$(v) is
\\[0ex]$P$ s v))
\-
\end{tabbing}